#!/bin/bash

if [ ${NO_CHECK}"x" == "1x" ]; then
  # disable check for performance monitoring
  exit 0
fi

TEMP=$(getopt -o r::,i::,l::,d --long reference::,implementation::,cell_library::,top::,yosys:: -n 'lgcheck' -- "$@")
eval set -- "$TEMP"

if [ -x "bazel-bin/inou/yosys/yosys2" ]; then
  YOSYS="./bazel-bin/inou/yosys/yosys2"
elif [ -x "inou/yosys/yosys2" ]; then
  YOSYS="inou/yosys/yosys2"
elif [ -x "lgshell.runfiles/livehd/inou/yosys/yosys2" ]; then
  YOSYS="lgshell.runfiles/livehd/inou/yosys/"
else
  YOSYS=$(which yosys)
fi


CELLLIB=""
OPT_TOP=""
OPT_DEBUG=""
LIST_SET=""
GOLD=""
GATE=""
while true ; do
    case "$1" in
        -r|--reference)
          case "$2" in
              "") shift 2 ;;
              *) GOLD=$2 ; shift 2 ;;
          esac ;;
        -i|--implementation)
          case "$2" in
              "") shift 2 ;;
              *) GATE=$2 ; shift 2 ;;
          esac ;;
        -l|--cell_library)
          case "$2" in
              "") shift 2 ;;
              *) CELLLIB=$2 ; shift 2 ;;
          esac ;;
        --yosys)
          case "$2" in
              "") shift 2 ;;
              *) YOSYS=$2 ; shift 2 ;;
          esac ;;
        --top)
          case "$2" in
              "") shift 2 ;;
              *) OPT_TOP=$2 ; shift 2 ;;
          esac ;;
        -d)
          shift 1 ;
          OPT_DEBUG=1 ;;
        --)
          LIST_SET="true"
          shift
          break
          ;;
        *)
          echo "Option $1 not recognized!"
          exit 1
          ;;
    esac
done

if [ "${LIST_SET}" == "true" ]; then
  for var in "$@"
  do
    if [ "${GOLD}" == "" ]; then
      GOLD=$var
      echo "setting GOLD:$GOLD"
    elif [ "${GATE}" == "" ]; then
      GATE=$var
      echo "setting GATE:$GATE"
    else
      echo "Too many files to check"
      exit 3
    fi
  done
fi

if [ "${GATE}" == "" ]; then
  echo "implementation circuit not provided"
  exit 1
fi

if [ ! -f ${GOLD} ]; then
  echo "reference circuit file not found"
  exit 1
fi

if [ ! -f ${GATE} ]; then
  if [ -d ${GATE} ] ; then
    GATE=${GATE}/*
    echo "using directory ${GATE}"
  else
    echo "implementation circuit file not found"
    exit 1
  fi
fi

if [ ! -f "${YOSYS}" ]; then
  if [ -x "/usr/bin/yosys" ]; then
    YOSYS=/usr/bin/yosys
  elif [ -x "/usr/local/bin/yosys" ]; then
    YOSYS=/usr/local/bin/yosys
  else
    echo "lgcheck: unable to fix YOSYS path"
    exit 5
  fi
fi

fm_top=$OPT_TOP
if [ "${fm_top}" == "" ]; then
  filename=$(basename -- "$GATE")
  fm_top="${filename%.*}"
  if [[ $fm_top =~ "long_" ]]; then
    fm_top=${fm_top:5}
  elif [[ $fm_top =~ "fixme_" ]]; then
    fm_top=${fm_top:6}
  fi
fi

if [ -z $FM_SHELL ]; then
  FM_SHELL=$(which fm_shell)
fi

if [ -x "${FM_SHELL}" ]; then
  echo "using formality"

  echo "
  set_app_var synopsys_auto_setup true
  set_app_var hdlin_ignore_parallel_case false
  set_app_var hdlin_ignore_full_case false
  read_sverilog -r  \"${GOLD}\"
  set_top ${fm_top}
  read_sverilog -i  \"${GATE}\"
  set_top ${fm_top}
  match
  report_unmatched_points >> \"fm_${fm_top}_error.log\"
  if { ![verify] }  {
    report_failing_points >> \"fm_${fm_top}_error.log\"
    report_aborted >> \"fm_${fm_top}_error.log\"
    analyze_points -all >> \"fm_${fm_top}_error.log\"
  }
  exit
  " > fm_script_${fm_top}.tcl

  ${FM_SHELL} -64bit -f fm_script_${fm_top}.tcl | grep "Verification SUCCEEDED"
  if [ $? -eq 0 ]; then
    echo "5.Successfully matched ${GATE} with ${GOLD} top:${fm_top}"
    exit 0
  fi

  echo "WARN: formality failed to prove equivalency."
fi

echo "using yosys:"${YOSYS}

if [ ! -f ${YOSYS} ]; then
  echo "Yosys binary not found"
  exit 1
fi

TOP_STR="-auto-top"
if [ "${OPT_TOP}" != "" ]; then
  TOP_STR="-top $OPT_TOP"
fi

echo "checking GATE:$GATE vs GOLD:$GOLD with top:$OPT_TOP directory:$PWD"

if [ "${CELLLIB}" != "" ]; then
  if [ ! -f ${CELLLIB} ]; then
    echo "cell library ${CELLLIB} not found"
    exit 1
  fi
  lib="read_verilog -sv ${CELLLIB}"
fi

#exit 2

yosys_read="read_verilog -sv ${GOLD}; hierarchy ${TOP_STR}; proc; flatten; rename -top gold; design -stash gold;
            read_verilog -sv ${GATE}; hierarchy ${TOP_STR}; proc; flatten; rename -top gate; design -stash gate;
            design -copy-from gold -as gold gold; design -copy-from gate -as gate gate; ${lib};"

yosys_prep="proc; memory -nomap; write_verilog trace0.v ; equiv_make gold gate equiv; write_verilog trace0b.v ; prep -flatten -top equiv; hierarchy -top equiv; hierarchy -check; flatten; proc; opt_clean;"

yosys_equiv="equiv_simple;"
#yosys_equiv_extra="${yosys_simple}; equiv_simple -seq 4; equiv_induct -seq 4;"
yosys_equiv_extra="${yosys_simple}; equiv_induct -seq 4;"

#try fast script first, if it fails, goes to more complex one
if [ "$OPT_DEBUG" != "" ]; then
  echo "${YOSYS} -p \"${yosys_read}; ${yosys_prep}; ${yosys_equiv}; equiv_status -assert\""
fi

${YOSYS} -p "${yosys_read}; ${yosys_prep}; ${yosys_equiv}; write_verilog trace1.v ; equiv_status -assert" \
    2> /dev/null | tee lgcheck1.log | grep "Equivalence successfully proven!"

if [ $? -eq 0 ]; then
  echo "1.Successfully matched ${GATE} with ${GOLD} top:${OPT_TOP}"
  exit 0
fi

#${YOSYS} -p " read_verilog -sv ${GOLD}; hierarchy ${TOP_STR}; opt ; prep; memory; rename -top gold; design -stash gold;
              #read_verilog -sv ${GATE}; hierarchy ${TOP_STR}; opt ; prep; memory; rename -top gate; design -stash gate;
              #design -copy-from gold -as gold gold
              #design -copy-from gate -as gate gate
#
              #miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
              #hierarchy -top equiv
              #sat -prove-asserts -tempinduct -timeout 30 -ignore_unknown_cells -verify -set-init-undef equiv" \
#    2> /dev/null | grep "Equivalence successfully proven!"
#if [ $? -eq 0 ]; then
#  echo "Successfully matched ${GATE} with ${GOLD} top:${OPT_TOP}"
#  exit 0
#fi

if grep -q reset ${GOLD}
then
  RESET_STMT="-set in_reset 1 -set-at 2 in_reset 0"
else
  RESET_STMT=""
fi

${YOSYS} -p " read_verilog -sv ${GOLD}; hierarchy ${TOP_STR}; opt; flatten ; rename -top gold; prep -top gold ; design -stash gold;
              read_verilog -sv ${GATE}; hierarchy ${TOP_STR}; opt; flatten ; rename -top gate; prep -top gate ; design -stash gate;
              design -copy-from gold -as gold gold
              design -copy-from gate -as gate gate

              miter -equiv -flatten -make_outputs -ignore_gold_x gold gate miter
              hierarchy -top miter
              write_verilog trace2.v
              sat -tempinduct -prove trigger 0 ${RESET_STMT} -set-init-undef -enable_undef -set-def-inputs -ignore_unknown_cells -show-ports miter
              " \
    2> /dev/null | tee lgcheck2.log | grep "proven: SUCC"
if [ $? -eq 0 ]; then
  echo "2.Successfully matched ${GATE} with ${GOLD} top:${OPT_TOP}"
  exit 0
fi

#${YOSYS} -p "${yosys_read};
#    proc; memory -nomap; opt_expr -full; opt -purge; opt -purge;
#    opt_reduce -full; opt_expr -mux_undef; opt_reduce; opt_merge; opt_clean -purge;
#    ${yosys_prep}; opt -purge; proc; opt -purge; ${yosys_equiv}; equiv_status -assert" 
#
#if [ $? -eq 0 ]; then
#  echo "3.Successfully matched ${GATE} with ${GOLD} top:${OPT_TOP}"
#  exit 0
#fi

${YOSYS} -p "${yosys_read};
    memory -nomap; opt_expr -full; opt -purge; proc; opt -purge;
    opt_reduce -full; opt_expr -mux_undef; opt_reduce; opt_merge; opt_clean -purge; techmap -map +/adff2dff.v;
    ${yosys_prep}; opt -purge; proc; opt -purge; ${yosys_equiv_extra}; equiv_status -assert" \
    2>/dev/null | tee lgcheck4.log | grep "Equivalence successfully proven!"

if [ $? -eq 0 ]; then
  echo "4.Successfully matched ${GATE} with ${GOLD} top:${OPT_TOP}"
  exit 0
fi

echo "WARN: Yosys failed to prove equivalency."

echo "FAIL: circuits are not equivalent ${GATE} vs ${GOLD} with top:${fm_top}"
exit 1
